the_es:event_system{i:l}, j,e:es-E(the_es).
(es-first(the_es; j))  (es-locl(the_es; e; j)) 

latex

Definitions	x:A. B(x), P  Q, t  T, P  Q, P  Q, prop{i:l}
Lemmas	es-axioms, assert wf, es-first wf, es-E wf, event system wf